Avoid wildcard expansion when making F# builds #3421
Conversation
This fixes a regression introduced in FStarLang@af1b98d Before the regression there was the term: --already_cached '*,' The regression switched it to: --already_cached '*' which causes: Y:/source/FStar/src/ocaml-output/fstar/bin/fstar.exe --use_hints --warn_error @241 --cache_checked_modules --odir fs/extracted --cache_dir .cache --already_cached '*' FStar.Pervasives.fst --codegen FSharp --extract_module FStar.Pervasives * Error 151: - Not a valid FStar file: '..' 1 error was reported (see above) make: *** [Makefile.extract.fsharp:34: fs/extracted/FStar_Pervasives.fs] Error 1 This fix puts back the original trailing comma which inhibits the wildcard expansion.
|
Hi Jonah, thanks for this! And sorry I broke it... How is this being expanded? Is it running on powershell maybe? Bash and other Unix shells wouldn't expand under the single quotes. Patch is good in any case, just curious. Thanks! |
|
Yes, So it could be PowerShell or Command Prompt that is seeing the However, Command Prompt (DOS) itself does not expand wildcards. Unlike Unix, the entire command line argument string is given to the executable (ex. |
|
From what Jonathan Protzenko told me back then, Windows expands wildcards even with |
|
Small world. I think the |
Yes, he uses |
|
Glad that I'll be remembered on the internet for digging into the shell expansion semantics of Cygwin vs native programs. See also https://stackoverflow.com/questions/9946586/cygwin-bash-c-yields-different-argc-depending-on-whether-the-command-start-with for another entry that I hope will make it into my collected works. |
This fixes a regression introduced in af1b98d. It was discovered testing Windows CI in #3402 and is a blocker for that PR.
Before the regression there was the term:
The regression switched it to:
which causes:
This fix puts back the original trailing comma which inhibits the wildcard expansion.